A:Type, eq:EqDecider(A), B:(AType), f:x:A fp B(x), P:(x:{x:A| x  dom(f) }B(x)Prop).
xdom(f). v=f(x)   P(x,v)  Prop 

latex

Definitions	x:A. B(x), x(s), Prop, t  T, xdom(f). v=f(x)   P(x;v), x(s1,s2), P  Q, x. t(x)
Lemmas	assert wf, fpf-dom wf, fpf-trivial-subtype-top, fpf-ap wf, fpf wf, deq wf